FDL - Nuprl Lemma : ma-interface-valtype

Nuprl Lemma : ma-interface-valtype_wf

11,40

A:Type, I:MaInterface(A), i:Id.
(i

ma-interface-locs(I))

(

k:Knd. (k

ma-interface-dom(I;i))

(ma-interface-valtype(I;i;k)

Type))

Definitions Knd, (x l), P Q, x:A. B(x), Id, MaInterface(T), Type, ma-interface-valtype(I;i;k)